REF, NoConds \\[0ex]Decide $a$ $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$Decide $a$ $\cdot$